{-# LANGUAGE NondecreasingIndentation #-}

module Agda.TypeChecking.Records where

import Prelude hiding (null)

import Control.Applicative        ( (<|>) )
import Control.Monad.Except       ( MonadError )
import Control.Monad.Trans.Maybe  ( MaybeT(MaybeT), runMaybeT )
import Control.Monad.Writer       ( Writer, runWriter, tell )

import Data.Bifunctor
import qualified Data.List as List
import Data.Maybe
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.HashMap.Strict as HMap

import Agda.Syntax.Common
import qualified Agda.Syntax.Concrete.Name as C
import Agda.Syntax.Concrete (FieldAssignment'(..))
import Agda.Syntax.Abstract.Name
import Agda.Syntax.Internal.MetaVars (unblockOnAnyMetaIn)
import Agda.Syntax.Internal as I
import Agda.Syntax.Position
import Agda.Syntax.Scope.Base (isNameInScope)

import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.Monad
import qualified Agda.TypeChecking.Monad.Base.Warning as W
import Agda.TypeChecking.Pretty as TCM
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Reduce.Monad () --instance only
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Warnings
import {-# SOURCE #-} Agda.TypeChecking.Primitive.Cubical.Base (isCubicalSubtype)
import {-# SOURCE #-} Agda.TypeChecking.ProjectionLike (eligibleForProjectionLike)

import Agda.Utils.CallStack ( HasCallStack )
import Agda.Utils.Empty
import Agda.Utils.Function (applyWhen)
import Agda.Utils.Functor (for, ($>), (<&>))
import Agda.Utils.Lens
import Agda.Utils.List
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Syntax.Common.Pretty (prettyShow)
import Agda.Utils.Singleton
import Agda.Utils.Size

import Agda.Utils.Impossible

---------------------------------------------------------------------------
-- * Tools to build record values

mkCon :: ConHead -> ConInfo -> Args -> Term
mkCon h info args = Con h info (map Apply args)

-- | Order the fields of a record construction.
orderFields
  :: forall a . HasRange a
  => ConOrigin         -- ^ Indicates whether this is a @record@ or @record where@ expression.
  -> QName             -- ^ Name of record type (for error message).
  -> (Arg C.Name -> a) -- ^ How to fill a missing field.
  -> [Arg C.Name]      -- ^ Field names of the record type.
  -> [(C.Name, a)]     -- ^ Provided fields with content in the record expression.
  -> Writer [RecordFieldWarning] [a]           -- ^ Content arranged in official order.
orderFields orig r fill axs fs = do
  -- reportSDoc "tc.record" 30 $ vcat
  --   [ "orderFields"
  --   , "  official fields: " <+> sep (map pretty xs)
  --   , "  provided fields: " <+> sep (map pretty ys)
  --   ]
  unless (orig == ConORecWhere) $
    List1.unlessNull alien     $ warn $ W.TooManyFields r missing

  List1.unlessNull duplicate $ warn $ W.DuplicateFields . fmap (fmap pure)
  return $ for axs $ \ ax -> fromMaybe (fill ax) $ lookup (unArg ax) uniq
  where
    (uniq, duplicate) = nubAndDuplicatesOn fst fs   -- separating duplicate fields
    xs        = map unArg axs                       -- official fields (accord. record type)
    missing   = filter (not . hasElem (map fst fs)) xs  -- missing  fields
    alien     = filter (not . hasElem xs . fst) fs      -- spurious fields
    warn w    = tell . singleton . w . fmap (second getRange)

-- | Raise generated 'RecordFieldWarning's as warnings.
warnOnRecordFieldWarnings :: Writer [RecordFieldWarning] a -> TCM a
warnOnRecordFieldWarnings comp = do
  let (res, ws) = runWriter comp
  mapM_ (warning . RecordFieldWarning) ws
  return res

-- | Raise generated 'RecordFieldWarning's as errors.
failOnRecordFieldWarnings :: Writer [RecordFieldWarning] a -> TCM a
failOnRecordFieldWarnings comp = do
  let (res, ws) = runWriter comp
  mapM_ (typeError . recordFieldWarningToError) ws
    -- This will raise the first warning (if any) as error.
  return res

-- | Order the fields of a record construction.
--   Raise generated 'RecordFieldWarning's as warnings.
orderFieldsWarn
  :: forall a . HasRange a
  => ConOrigin         -- ^ Indicates whether this is a @record@ or @record where@ expression.
  -> QName             -- ^ Name of record type (for error message).
  -> (Arg C.Name -> a) -- ^ How to fill a missing field.
  -> [Arg C.Name]      -- ^ Field names of the record type.
  -> [(C.Name, a)]     -- ^ Provided fields with content in the record expression.
  -> TCM [a]           -- ^ Content arranged in official order.
orderFieldsWarn o r fill axs fs = warnOnRecordFieldWarnings $ orderFields o r fill axs fs

-- | Order the fields of a record construction.
--   Raise generated 'RecordFieldWarning's as errors.
orderFieldsFail
  :: forall a . HasRange a
  => ConOrigin         -- ^ Indicates whether this is a @record@ or @record where@ expression.
  -> QName             -- ^ Name of record type (for error message).
  -> (Arg C.Name -> a) -- ^ How to fill a missing field.
  -> [Arg C.Name]      -- ^ Field names of the record type.
  -> [(C.Name, a)]     -- ^ Provided fields with content in the record expression.
  -> TCM [a]           -- ^ Content arranged in official order.
orderFieldsFail o r fill axs fs = failOnRecordFieldWarnings $ orderFields o r fill axs fs

-- | A record field assignment @record{xs = es}@ might not mention all
--   visible fields.  @insertMissingFields@ inserts placeholders for
--   the missing visible fields and returns the values in order
--   of the fields in the record declaration.
insertMissingFields
  :: forall a . HasRange a
  => ConOrigin            -- ^ Indicates whether this is a @record@ or @record where@ expression.
  -> QName                -- ^ Name of record type (for error reporting).
  -> (C.Name -> a)        -- ^ Function to generate a placeholder for missing visible field.
  -> [FieldAssignment' a] -- ^ Given fields.
  -> [Arg C.Name]         -- ^ All record field names with 'ArgInfo'.
  -> Writer [RecordFieldWarning] [NamedArg a]
       -- ^ Given fields enriched by placeholders for missing explicit fields.
insertMissingFields o r placeholder fs axs = do
  -- Compute the list of given fields, decorated with the ArgInfo from the record def.
  let arg x e = caseMaybe (List.find ((x ==) . unArg) axs) (defaultNamedArg e) $ \ a ->
        nameIfHidden a e <$ a
      givenFields = [ (x, Just $ arg x e) | FieldAssignment x e <- fs ]

  -- Omitted explicit fields are filled in with placeholders.
  -- Omitted implicit or instance fields
  -- are still left out and inserted later by checkArguments_.
  catMaybes <$> orderFields o r fill axs givenFields
  where
    fill :: Arg C.Name -> Maybe (NamedArg a)
    fill ax
      | visible ax = Just $ setOrigin Inserted $ unnamed . placeholder <$> ax
      | otherwise  = Nothing
    -- Andreas, 2017-04-13, issue #2494
    -- We need to put the field names as argument names for hidden arguments.
    -- Otherwise, insertImplicit does not do the right thing.
    nameIfHidden :: Arg C.Name -> c -> Named_ c
    nameIfHidden ax
      | visible ax = unnamed
      | otherwise  = named $ WithOrigin Inserted $ Ranged (getRange ax) $ prettyShow $ unArg ax

-- | A record field assignment @record{xs = es}@ might not mention all
--   visible fields.  @insertMissingFields@ inserts placeholders for
--   the missing visible fields and returns the values in order
--   of the fields in the record declaration.
insertMissingFieldsWarn
  :: forall a . HasRange a
  => ConOrigin            -- ^ Indicates whether this is a @record@ or @record where@ expression.
  -> QName                -- ^ Name of record type (for error reporting).
  -> (C.Name -> a)        -- ^ Function to generate a placeholder for missing visible field.
  -> [FieldAssignment' a] -- ^ Given fields.
  -> [Arg C.Name]         -- ^ All record field names with 'ArgInfo'.
  -> TCM [NamedArg a]     -- ^ Given fields enriched by placeholders for missing explicit fields.
insertMissingFieldsWarn o r placeholder fs axs =
  warnOnRecordFieldWarnings $ insertMissingFields o r placeholder fs axs

-- | A record field assignment @record{xs = es}@ might not mention all
--   visible fields.  @insertMissingFields@ inserts placeholders for
--   the missing visible fields and returns the values in order
--   of the fields in the record declaration.
insertMissingFieldsFail
  :: forall a . HasRange a
  => ConOrigin            -- ^ Indicates whether this is a @record@ or @record where@ expression.
  -> QName                -- ^ Name of record type (for error reporting).
  -> (C.Name -> a)        -- ^ Function to generate a placeholder for missing visible field.
  -> [FieldAssignment' a] -- ^ Given fields.
  -> [Arg C.Name]         -- ^ All record field names with 'ArgInfo'.
  -> TCM [NamedArg a]     -- ^ Given fields enriched by placeholders for missing explicit fields.
insertMissingFieldsFail o r placeholder fs axs =
  failOnRecordFieldWarnings $ insertMissingFields o r placeholder fs axs

---------------------------------------------------------------------------
-- * Query information about records from signature

-- | Check if a name refers to a record.
--   If yes, return record definition.
{-# SPECIALIZE isRecord :: HasCallStack => QName -> TCM (Maybe RecordData) #-}
{-# SPECIALIZE isRecord :: HasCallStack => QName -> ReduceM (Maybe RecordData) #-}
isRecord :: (HasCallStack, HasConstInfo m) => QName -> m (Maybe RecordData)
isRecord r = do
  getConstInfo r <&> theDef <&> \case
    RecordDefn rd -> Just rd
    _ -> Nothing

-- | Get the definition for a record. Throws an exception if the name
--   does not refer to a record or the record is abstract.
getRecordDef :: (HasCallStack, HasConstInfo m, ReadTCState m, MonadError TCErr m) => QName -> m RecordData
getRecordDef r = fromMaybeM err $ isRecord r
  where err = typeError $ ShouldBeRecordType (El __DUMMY_SORT__ $ Def r [])

-- | Get the record name belonging to a field name.
getRecordOfField :: HasCallStack => QName -> TCM (Maybe QName)
getRecordOfField d = caseMaybeM (isProjection d) (return Nothing) $
  \ Projection{ projProper = proper, projFromType = r} ->
    return $ unArg r <$ proper -- if proper then Just (unArg r) else Nothing

-- | Get the field names of a record.
getRecordFieldNames :: (HasCallStack, HasConstInfo m, ReadTCState m, MonadError TCErr m)
  => QName
  -> m [Dom C.Name]
getRecordFieldNames r = recordFieldNames <$> getRecordDef r

recordFieldNames :: RecordData -> [Dom C.Name]
recordFieldNames = map (fmap (nameConcrete . qnameName)) . _recFields

-- | Find all records with at least the given fields.
findPossibleRecords :: [C.Name] -> TCM [QName]
findPossibleRecords fields = do
  defs  <- HMap.elems <$> useTC (stSignature . sigDefinitions)
  idefs <- HMap.elems <$> useTC (stImports   . sigDefinitions)
  scope <- getScope
  return $ filter (`isNameInScope` scope) $ cands defs ++ cands idefs
  where
    cands defs = [ defName d | d <- defs, possible d ]
    possible def =
      -- Check whether the given fields are contained
      -- in the fields of record @def@ (if it is a record).
      case theDef def of
        Record{ recFields = fs } -> Set.isSubsetOf given $
          Set.fromList $ map (nameConcrete . qnameName . unDom) fs
        _ -> False
    given = Set.fromList fields

-- | Get the field names belonging to a record type.
getRecordTypeFields :: HasCallStack
  => Type  -- ^ Record type.  Need not be reduced.
  -> TCM [Dom QName]
getRecordTypeFields t = do
  t <- reduce t  -- Andreas, 2018-03-03, fix for #2989.
  case unEl t of
    Def r _ -> do
      rDef <- theDef <$> getConstInfo r
      case rDef of
        Record { recFields = fields } -> return fields
        _ -> __IMPOSSIBLE__
    _ -> __IMPOSSIBLE__

-- | Returns the given record type's constructor name (with an empty
-- range).
getRecordConstructor :: (HasCallStack, HasConstInfo m, ReadTCState m, MonadError TCErr m) => QName -> m ConHead
getRecordConstructor r = killRange . _recConHead <$> getRecordDef r

-- | Reduce a type and check whether it is a record type.
--   Succeeds only if type is not blocked by a meta var.
--   If yes, return its name, parameters, and definition.
isRecordType :: (HasCallStack, PureTCM m) => Type -> m (Maybe (QName, Args, RecordData))
isRecordType t = either (const Nothing) Just <$> tryRecordType t

-- | Reduce a type and check whether it is a record type.
--   Succeeds only if type is not blocked by a meta var.
--   If yes, return its name, parameters, and definition.
--   If no, return the reduced type (unless it is blocked).
tryRecordType :: (HasCallStack, PureTCM m) => Type -> m (Either (Blocked Type) (QName, Args, RecordData))
tryRecordType t = ifBlocked t (\ m a -> return $ Left $ Blocked m a) $ \ nb t -> do
  let no = return $ Left $ NotBlocked nb t
  case unEl t of
    Def r es -> do
      let vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
      caseMaybeM (isRecord r) no $ \ def -> return $ Right (r,vs,def)
    _ -> no

-- | Get the original projection info for name.
{-# SPECIALIZE origProjection :: HasCallStack => QName -> TCM (QName, Definition, Maybe Projection) #-}
origProjection ::  (HasCallStack, HasConstInfo m) => QName -> m (QName, Definition, Maybe Projection)
origProjection f = do
  def <- getConstInfo f
  let proj     = isProjection_ $ theDef def
      fallback = return (f, def, proj)
  caseMaybe proj fallback $
    \ p@Projection{ projProper = proper, projOrig = f' } ->
      if isNothing proper || f == f' then fallback else do
        def <- getConstInfo f'
        return (f', def, isProjection_ $ theDef def)

-- | @getDefType f t@ computes the type of (possibly projection-(like))
--   function @f@ whose first argument has type @t@.
--   The `parameters' for @f@ are extracted from @t@.
--   @Nothing@ if @f@ is projection(like) but
--   @t@ is not a data/record/axiom type.
--
--   Precondition: @t@ is reduced.
--
--   See also: 'Agda.TypeChecking.Datatypes.getConType'
getDefType :: PureTCM m => QName -> Type -> m (Maybe Type)
getDefType f t = do
  -- Andreas, Issue #1973: we need to take the original projection
  -- since the parameters from the reduced type t are correct for
  -- the original projection only.
  -- Due to module application, the given (non-original) projection f
  -- may expect less parameters, those corresponding to a unreduced
  -- version of t (which we cannot obtain here).
  (f, def, mp) <- origProjection f
  let a = defType def
  -- if @f@ is not a projection (like) function, @a@ is the correct type
      fallback = return $ Just a
  reportSDoc "tc.deftype" 20 $ vcat
    [ "definition f =" <+> prettyTCM f <+> text ("  -- raw: " ++ prettyShow f)
    , "has type   a =" <+> prettyTCM a
    , "principal  t =" <+> prettyTCM t
    ]
  caseMaybe mp fallback $
    \ (Projection{ projIndex = n }) -> if n <= 0 then fallback else do
      -- otherwise, we have to instantiate @a@ to the "parameters" of @f@
      let npars | n == 0    = __IMPOSSIBLE__
                | otherwise = n - 1
      reportSLn "tc.deftype" 20 $ "projIndex    = " ++ show n
      -- we get the parameters from type @t@
      case unEl t of
        Def d es -> do
          -- Andreas, 2013-10-22
          -- we need to check this @Def@ is fully reduced.
          -- If it is stuck due to disabled reductions
          -- (because of failed termination check),
          -- we will produce garbage parameters.
          ifNotM (eligibleForProjectionLike d) failNotElig $ {- else -} do
            -- now we know it is reduced, we can safely take the parameters
            let pars = fromMaybe __IMPOSSIBLE__ $ allApplyElims $ take npars es
            reportSDoc "tc.deftype" 20 $ vcat
              [ text $ "head d     = " ++ prettyShow d
              , "parameters =" <+> sep (map prettyTCM pars)
              ]
            reportSDoc "tc.deftype" 60 $ "parameters = " <+> pretty pars
            if length pars < npars then failure "does not supply enough parameters"
            else Just <$> a `piApplyM` pars
        _ -> failNotDef
  where
    failNotElig = failure "is not eligible for projection-likeness"
    failNotDef  = failure "is not a Def."
    failure reason = do
      reportSDoc "tc.deftype" 25 $ sep
        [ "Def. " <+> prettyTCM f <+> " is projection(like)"
        , "but the type "
        , prettyTCM t
        , text $ "of its argument " ++ reason
        ]
      reportSDoc "tc.deftype" 60 $ "raw type: " <+> pretty t
      return $ case unEl t of
        Dummy{} -> Just __DUMMY_TYPE__
        _       -> Nothing

-- | Apply a projection to an expression with a known type, returning
--   the type of the projected value.
--   The given type should either be a record type or a type eligible for
--   the principal argument of a projection-like function.
shouldBeProjectible :: (PureTCM m, MonadTCError m, MonadBlock m)
                    => Term -> Type -> ProjOrigin -> QName -> m Type
-- shouldBeProjectible t f = maybe failure return =<< projectionType t f
shouldBeProjectible v t o f = do
  t <- abortIfBlocked t
  projectTyped v t o f >>= \case
    Just (_ , _ , ft) -> return ft
    Nothing -> case t of
      El _ Dummy{} -> return __DUMMY_TYPE__
      _ -> typeError $ ShouldBeRecordType t
    -- TODO: more accurate error that makes sense also for proj.-like funs.

-- | The analogue of 'piApply'.  If @v@ is a value of record type @t@
--   with field @f@, then @projectTyped v t f@ returns the type of @f v@.
--   And also the record type (as first result).
--
--   Works also for projection-like definitions @f@.
--   In this case, the first result is not a record type.
--
--   Precondition: @t@ is reduced.
--
projectTyped
  :: PureTCM m
  => Term        -- ^ Head (record value).
  -> Type        -- ^ Its type.
  -> ProjOrigin
  -> QName       -- ^ Projection.
  -> m (Maybe (Dom Type, Term, Type))
projectTyped v t o f = caseMaybeM (getDefType f t) (return Nothing) $ \ tf -> do
  ifNotPiType tf (const $ return Nothing) {- else -} $ \ dom b -> do
  u <- applyDef o f (argFromDom dom $> v)
  return $ Just (dom, u, b `absApp` v)

-- | Typing of an elimination.

data ElimType
  = ArgT (Dom Type)           -- ^ Type of the argument.
  | ProjT
    { projTRec   :: Dom Type  -- ^ The type of the record which is eliminated.
    , projTField :: Type      -- ^ The type of the field.
    }

instance PrettyTCM ElimType where
  prettyTCM (ArgT a)    = prettyTCM a
  prettyTCM (ProjT a b) =
    "." <> parens (prettyTCM a <+> "->" <+> prettyTCM b)

-- | Given a head and its type, compute the types of the eliminations.

typeElims :: Type -> Term -> Elims -> TCM [ElimType]
typeElims a _ [] = return []
typeElims a self (e : es) = do
  case e of
    -- Andrea 02/08/2017: when going from patterns to elims we
    -- generate an Apply elim even for Path types, because we use VarP
    -- for both, so we have to allow for a Path type here.
    Apply v -> ifNotPiOrPathType a __IMPOSSIBLE__ {- else -} $ \ a b -> do
      (ArgT a :) <$> typeElims (absApp b $ unArg v) (self `applyE` [e]) es
    Proj o f -> do
      a <- reduce a
      (dom, self, a) <- fromMaybe __IMPOSSIBLE__ <$> projectTyped self a o f
      (ProjT dom a :) <$> typeElims a self es
    IApply{} -> __IMPOSSIBLE__

-- | Given a term with a given type and a list of eliminations, returning the
--   type of the term applied to the eliminations.
eliminateType :: (PureTCM m) => m Empty -> Term -> Type -> Elims -> m Type
eliminateType err = eliminateType' err . applyE

eliminateType' :: (PureTCM m) => m Empty -> (Elims -> Term) -> Type -> Elims -> m Type
eliminateType' err hd t [] = return t
eliminateType' err hd t (e : es) = case e of
  Apply v -> do
    t' <- piApplyM' err t v
    eliminateType' err (hd . (e:)) t' es
  Proj o f -> reduce t >>= getDefType f >>= \case
    Just a -> ifNotPiType a (\_ -> absurd <$> err) $ \_ c ->
      eliminateType' err (hd . (e:)) (c `absApp` (hd [])) es
    Nothing -> absurd <$> err
  IApply _ _ r -> do
    t' <- piApplyM' err t r
    eliminateType' err (hd . (e:)) t' es

-- | Check if a name refers to an eta expandable record.
--
-- The answer is no for a record type with an erased constructor
-- unless the current quantity is \"erased\".
{-# SPECIALIZE isEtaRecord :: HasCallStack => QName -> TCM Bool #-}
{-# SPECIALIZE isEtaRecord :: HasCallStack => QName -> ReduceM Bool #-}
isEtaRecord :: (HasCallStack, HasConstInfo m) => QName -> m Bool
isEtaRecord r = do
  isRecord r >>= \case
    Just r | isEtaRecordDef r -> do
     constructorQ <- getQuantity <$> getConstInfo (conName (_recConHead r))
     currentQ     <- viewTC eQuantity
     return $ constructorQ `moreQuantity` currentQ
    _ -> return False

isEtaRecordDef :: RecordData -> Bool
isEtaRecordDef r = _recEtaEquality r == YesEta

{-# INLINE isEtaCon #-}
isEtaCon :: (HasCallStack, HasConstInfo m) => QName -> m Bool
isEtaCon c = isJust <$> isEtaRecordConstructor c

-- | Going under one of these does not count as a decrease in size for the termination checker.
isEtaOrCoinductiveRecordConstructor :: (HasCallStack, HasConstInfo m) => QName -> m Bool
isEtaOrCoinductiveRecordConstructor c =
  caseMaybeM (isRecordConstructor c) (return False) $ \ (_, def) ->
    pure (isEtaRecordDef def) `or2M`
      return (_recInduction def /= Just Inductive)
      -- If in doubt about coinductivity, then yes.

-- | Check if a name refers to a record which is not coinductive.  (Projections are then size-preserving)
isInductiveRecord :: (HasCallStack, HasConstInfo m) => QName -> m Bool
isInductiveRecord r = maybe False ((Just CoInductive /=) . _recInduction) <$> isRecord r

-- | Check if a type is an eta expandable record and return the record identifier and the parameters.
isEtaRecordType :: (HasCallStack, HasConstInfo m)
  => Type
  -> m (Maybe (QName, Args))
isEtaRecordType a = case unEl a of
  Def d es -> do
    let vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
    ifM (isEtaRecord d) (return $ Just (d, vs)) (return Nothing)
  _        -> return Nothing

-- | Check if a name refers to a record constructor.
--   If yes, return record definition.
--
isRecordConstructor :: (HasCallStack, HasConstInfo m) => QName -> m (Maybe (QName, RecordData))
isRecordConstructor c = getConstInfo' c >>= \case
  Left (SigUnknown err)     -> __IMPOSSIBLE_VERBOSE__ err
  Left SigCubicalNotErasure -> __IMPOSSIBLE__
  Left SigAbstract          -> return Nothing
  Right def                 -> case theDef $ def of
    Constructor{ conData = r } -> fmap (r,) <$> isRecord r
    _                          -> return Nothing

isEtaRecordConstructor :: (HasCallStack, HasConstInfo m) => QName -> m (Maybe (QName, RecordData))
isEtaRecordConstructor c = isRecordConstructor c >>= \case
  Nothing -> return Nothing
  Just (d, def) -> if isEtaRecordDef def then return $ Just (d, def) else return Nothing

-- | Turn off eta for unguarded recursive records.
--   Projections do not preserve guardedness.
unguardedRecord :: QName -> PatternOrCopattern -> TCM ()
unguardedRecord q pat = modifyRecEta q \ eta -> setEtaEquality eta $ NoEta pat

-- | Turn on eta for non-recursive and inductive guarded recursive records,
--   unless user declared otherwise.
--   Projections do not preserve guardedness.
updateEtaForRecord :: QName -> TCM ()
updateEtaForRecord q = whenM etaEnabled $ do

  -- Do we need to switch on eta for record q?
  switchEta <- getConstInfo q <&> theDef <&> \case
    Record{ recInduction = ind, recEtaEquality' = eta }
      | Inferred NoEta{} <- eta, ind /= Just CoInductive -> True
      | otherwise -> False
    _ -> __IMPOSSIBLE__

  when switchEta $ modifyRecEta q $ const $ Inferred YesEta

-- | Turn on eta for inductive guarded recursive records.
--   Projections do not preserve guardedness.
recursiveRecord :: QName -> TCM ()
recursiveRecord = updateEtaForRecord

-- | Turn on eta for non-recursive record, unless user declared otherwise.
nonRecursiveRecord :: QName -> TCM ()
nonRecursiveRecord = updateEtaForRecord

-- | Check whether record type is marked as recursive.
--
--   Precondition: record type identifier exists in signature.
isRecursiveRecord :: QName -> TCM Bool
isRecursiveRecord q =
  getSignature <&> lookupDefinition q <&> fmap theDef <&> \case
    Just (RecordDefn r) -> recRecursive_ r
    _ -> __IMPOSSIBLE__

{- | @etaExpandBoundVar i = (Δ, σ, τ)@

Precondition: The current context is @Γ = Γ₁, x:R pars, Γ₂@ where
  @|Γ₂| = i@ and @R@ is a eta-expandable record type
  with constructor @c@ and fields @Γ'@.

Postcondition: @Δ = Γ₁, Γ', Γ₂[c Γ']@ and @Γ ⊢ σ : Δ@ and @Δ ⊢ τ : Γ@.
-}
etaExpandBoundVar :: Int -> TCM (Maybe (Telescope, Substitution, Substitution))
etaExpandBoundVar i = fmap (\ (delta, sigma, tau, _) -> (delta, sigma, tau)) <$> do
  expandRecordVar i =<< getContextTelescope

-- | @expandRecordVar i Γ = (Δ, σ, τ, Γ')@
--
--   Precondition: @Γ = Γ₁, x:R pars, Γ₂@ where
--     @|Γ₂| = i@ and @R@ is a eta-expandable record type
--     with constructor @c@ and fields @Γ'@.
--
--   Postcondition: @Δ = Γ₁, Γ', Γ₂[c Γ']@ and @Γ ⊢ σ : Δ@ and @Δ ⊢ τ : Γ@.

expandRecordVar :: PureTCM m => Int -> Telescope -> m (Maybe (Telescope, Substitution, Substitution, Telescope))
expandRecordVar i gamma0 = do
  -- Get the context with last variable added last in list.
  let gamma = telToList gamma0
  -- Convert the de Bruijn index i to a de Bruijn level
      l     = size gamma - 1 - i
  -- Extract type of @i@th de Bruijn index.
  -- Γ = Γ₁, x:a, Γ₂
  let (gamma1, dom@(Dom{domInfo = ai, unDom = (x, a)}) : gamma2) = splitAt l gamma -- TODO:: Defined but not used dom, ai
  -- This must be a eta-expandable record type.
  let failure = do
        reportSDoc "tc.meta.assign.proj" 25 $
          "failed to eta-expand variable " <+> pretty x <+>
          " since its type " <+> prettyTCM a <+>
          " is not a record type"
        return Nothing
  caseMaybeM (isRecordType a) failure $ \ (r, pars, def) -> case isEtaRecordDef def of
    False -> return Nothing
    True  -> Just <$> do
      -- Get the record fields @Γ₁ ⊢ tel@ (@tel = Γ'@).
      -- TODO: compose argInfo ai with tel.
      let tel = _recTel def `apply` pars
          m   = size tel
          fs  = map argFromDom $ _recFields def
      -- Construct the record pattern @Γ₁, Γ' ⊢ u := c ys@.
          ys  = zipWith (\ f i -> f $> var i) fs $ downFrom m
          u   = mkCon (_recConHead def) ConOSystem ys
      -- @Γ₁, Γ' ⊢ τ₀ : Γ₁, x:_@
          tau0 = consS u $ raiseS m
      -- @Γ₁, Γ', Γ₂ ⊢ τ₀ : Γ₁, x:_, Γ₂@
          tau  = liftS (size gamma2) tau0

      --  Fields are in order first-first.
          zs  = for fs $ fmap $ \ f -> Var 0 [Proj ProjSystem f]
      --  We need to reverse the field sequence to build the substitution.
      -- @Γ₁, x:_ ⊢ σ₀ : Γ₁, Γ'@
          sigma0 = reverse (map unArg zs) ++# raiseS 1
      -- @Γ₁, x:_, Γ₂ ⊢ σ₀ : Γ₁, Γ', Γ₂@
          sigma  = liftS (size gamma2) sigma0

      -- Construct @Δ@ as telescope.
      -- Note @Γ₁, x:_ ⊢ Γ₂@, thus, @Γ₁, Γ' ⊢ [τ₀]Γ₂@

          -- Use "f(x)" as variable name for the projection f(x).
          s     = prettyShow x
          tel'  = mapAbsNames (\ f -> stringToArgName $ argNameToString f ++ "(" ++ s ++ ")") tel
          delta = telFromList $ gamma1 ++ telToList tel' ++
                    telToList (applySubst tau0 $ telFromList gamma2)
                    -- Andreas, 2017-07-29, issue #2644
                    -- We cannot substitute directly into a ListTel like gamma2,
                    -- we have to convert it to a telescope first, otherwise we get garbage.

      return (delta, sigma, tau, tel)

-- | Precondition: variable list is ordered descendingly.  Can be empty.
expandRecordVarsRecursively :: [Int] -> Telescope -> TCM (Telescope, Substitution, Substitution)
expandRecordVarsRecursively [] gamma = return (gamma, idS, idS)
expandRecordVarsRecursively (i : is) gamma = do
  caseMaybeM (expandRecordVar i gamma) (expandRecordVarsRecursively is gamma)
  $ \ (gamma1, sigma1, tau1, tel) -> do
    -- Γ ⊢ σ₁ : Γ₁  and  Γ₁ ⊢ τ₁ : Γ
    let n = size tel
        newis = take n $ downFrom $ i + n
    (gamma2, sigma2, tau2) <- expandRecordVarsRecursively (newis ++ is) gamma1
    -- Γ₁ ⊢ σ₂ : Γ₂  and  Γ₂ ⊢ τ₂ : Γ₁
    return (gamma2, applySubst sigma1 sigma2, applySubst tau2 tau1)

-- | @curryAt v (Γ (y : R pars) -> B) n =
--     ( \ v -> λ Γ ys → v Γ (c ys)            {- curry   -}
--     , \ v -> λ Γ y → v Γ (p1 y) ... (pm y)  {- uncurry -}
--     , Γ (ys : As) → B[c ys / y]
--     )@
--
--   where @n = size Γ@.
curryAt :: Type -> Int -> TCM (Term -> Term, Term -> Term, Type)
curryAt t n = do
  -- first, strip the leading n domains (which remain unchanged)
  TelV gamma core <- telViewUpTo n t
  case unEl core of
    -- There should be at least one domain left
    Pi (dom@Dom{domInfo = ai, unDom = a}) b -> do
      -- Eta-expand @dom@ along @qs@ into a telescope @tel@, computing a substitution.
      -- For now, we only eta-expand once.
      -- This might trigger another call to @etaExpandProjectedVar@ later.
      -- A more efficient version does all the eta-expansions at once here.
      (r, pars, def) <- fromMaybe __IMPOSSIBLE__ <$> isRecordType a
      if | NoEta _ <- _recEtaEquality def -> __IMPOSSIBLE__
         | otherwise -> return ()
      -- TODO: compose argInfo ai with tel.
      let tel = _recTel def `apply` pars
          m   = size tel
          fs  = map argFromDom $ _recFields def
          ys  = zipWith (\ f i -> f $> var i) fs $ downFrom m
          u   = mkCon (killRange $ _recConHead def) ConOSystem ys
          b'  = raise m b `absApp` u
          t'  = gamma `telePi` (tel `telePi` b')
          gammai = map domInfo $ telToList gamma
          xs  = reverse $ zipWith (\ ai i -> Arg ai $ var i) gammai [m..]
          curry v = teleLam gamma $ teleLam tel $
                      raise (n + m) v `apply` (xs ++ [Arg ai u])
          zs  = for fs $ fmap $ \ f -> Var 0 [Proj ProjSystem f]
          atel = sgTel $ (,) (absName b) <$> dom
          uncurry v = teleLam gamma $ teleLam atel $
                        raise (n + 1) v `apply` (xs ++ zs)
      return (curry, uncurry, t')
    _ -> __IMPOSSIBLE__

{-| @etaExpand r pars u@ computes the eta expansion of record value @u@
    at record type @r pars@.

    The first argument @r@ should be the name of an eta-expandable record type.
    Given

      @record R : Set where field x : A; y : B; .z : C@

    and @r : R@,

      @etaExpand R [] r = (tel, [R.x r, R.y r, R.z r])@

    where @tel@ is the record telescope instantiated at the parameters @pars@.
-}
etaExpandRecord :: (HasConstInfo m, MonadDebug m, ReadTCState m)
  => QName       -- ^ Name of record type.
  -> Args        -- ^ Parameters applied to record type.
  -> Term        -- ^ Term to eta-expand.
  -> m (Telescope, Args)
     -- ^ Field types instantiated to parameters, field values.
etaExpandRecord = etaExpandRecord' False

-- | Eta expand a record regardless of whether it's an eta-record or not.
forceEtaExpandRecord :: (HasConstInfo m, MonadDebug m, ReadTCState m, MonadError TCErr m)
  => QName       -- ^ Name of record type.
  -> Args        -- ^ Parameters applied to record type.
  -> Term        -- ^ Term to eta-expand.
  -> m (Telescope, Args)
     -- ^ Field types instantiated to parameters, field values.
forceEtaExpandRecord = etaExpandRecord' True

-- | Eta-expand a value at the given record type (must match).
etaExpandRecord' :: (HasConstInfo m, MonadDebug m, ReadTCState m)
  => Bool        -- ^ Force expansion, overriding '_recEtaEquality'?
  -> QName       -- ^ Name of record type.
  -> Args        -- ^ Parameters applied to record type.
  -> Term        -- ^ Term to eta-expand.
  -> m (Telescope, Args)
     -- ^ Field types instantiated to parameters, field values.
etaExpandRecord' forceEta r pars u = do
  def <- fromMaybe __IMPOSSIBLE__ <$> isRecord r
  (tel, _, _, args) <- etaExpandRecord'_ forceEta r pars def u
  return (tel, args)

-- | Eta-expand a value at the given eta record type (must match).
etaExpandRecord_ :: HasConstInfo m
  => QName       -- ^ Name of record type.
  -> Args        -- ^ Parameters applied to record type.
  -> RecordData  -- ^ Definition of record type.
  -> Term        -- ^ Term to eta-expand.
  -> m (Telescope, ConHead, ConInfo, Args)
     -- ^ Field types instantiated to parameters, disassembled constructor term.
etaExpandRecord_ = etaExpandRecord'_ False

-- | Eta-expand a value at the given record type (must match).
etaExpandRecord'_ :: HasConstInfo m
  => Bool        -- ^ Force expansion, overriding '_recEtaEquality'?
  -> QName       -- ^ Name of record type.
  -> Args        -- ^ Parameters applied to record type.
  -> RecordData  -- ^ Definition of record type.
  -> Term        -- ^ Term to eta-expand.
  -> m (Telescope, ConHead, ConInfo, Args)
     -- ^ Field types instantiated to parameters, disassembled constructor term.
etaExpandRecord'_ forceEta r pars
    def@RecordData{ _recConHead = con, _recFields = xs, _recTel = tel }
    u = do
  let tel' = apply tel pars
  -- Make sure we do not expand non-eta records (unless forced to):
  unless (_recEtaEquality def == YesEta || forceEta) __IMPOSSIBLE__
  case u of

    -- Already expanded.
    Con con_ ci es -> do
      let args = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
      -- Andreas, 2019-10-21, issue #4148
      -- @con == con_@ might fail, but their normal forms should be equal.
      whenNothingM (conName con `sameDef` conName con_) $ do
        reportSDoc "impossible" 10 $ vcat
          [ "etaExpandRecord_: the following two constructors should be identical"
          , nest 2 $ text $ "con  = " ++ prettyShow con
          , nest 2 $ text $ "con_ = " ++ prettyShow con_
          ]
        __IMPOSSIBLE__
      return (tel', con, ci, args)

    -- Not yet expanded.
    _ -> do
      -- Andreas, < 2016-01-18: Note: recFields are always the original projections,
      -- thus, we can use them in Proj directly.
      let xs' = for (map argFromDom xs) $ fmap $ \ x -> u `applyE` [Proj ProjSystem x]
      reportSDoc "tc.record.eta" 20 $ vcat
        [ "eta expanding" <+> prettyTCM u <+> ":" <+> prettyTCM r
        , nest 2 $ vcat
          [ "tel' =" <+> prettyTCM tel'
          , "args =" <+> prettyTCM xs'
          ]
        ]
      return (tel', con, ConOSystem, xs')

etaExpandAtRecordType :: Type -> Term -> TCM (Telescope, Term)
etaExpandAtRecordType t u = do
  (r, pars, def) <- fromMaybe __IMPOSSIBLE__ <$> isRecordType t
  (tel, con, ci, args) <- etaExpandRecord_ r pars def u
  return (tel, mkCon con ci args)

-- | The fields should be eta contracted already.
--
--   We can eta contract if all fields @f = ...@ are irrelevant
--   or all fields @f@ are the projection @f v@ of the same value @v@,
--   but we need at least one relevant field to find the value @v@.
--
--   If all fields are erased, we cannot eta-contract.

--   Andreas, 2019-11-06, issue #4168: eta-contraction all-erased record
--   lead to compilation error.

--   TODO: this can be moved out of TCM.
--   Andreas, 2018-01-28: attempted just that, but Auto does not
--   put the conFields there (it does not run in TCM).
--   If we get rid of Auto, we can do this.  (Tests not involving Auto pass.)

{-# SPECIALIZE etaContractRecord :: QName -> ConHead -> ConInfo -> Args -> TCM Term #-}
{-# SPECIALIZE etaContractRecord :: QName -> ConHead -> ConInfo -> Args -> ReduceM Term #-}
etaContractRecord :: HasConstInfo m => QName -> ConHead -> ConInfo -> Args -> m Term
etaContractRecord r c ci args = if all (not . usableModality) args then fallBack else do
  RecordData{ _recFields = xs } <- fromMaybe __IMPOSSIBLE__ <$> isRecord r
  reportSDoc "tc.record.eta.contract" 20 $ vcat
    [ "eta contracting record"
    , nest 2 $ vcat
      [ "record type r  =" <+> prettyTCM r
      , "constructor c  =" <+> prettyTCM c
      , "field names xs =" <+> pretty    xs
      , "fields    args =" <+> prettyTCM args
      ]
    ]
  case compare (length args) (length xs) of
    LT -> fallBack       -- Not fully applied
    GT -> __IMPOSSIBLE__ -- Too many arguments. Impossible.
    EQ -> do
      case zipWithM check args xs of
        Just as -> case catMaybes as of
          (a:as) ->
            if all (a ==) as
              then return a
              else fallBack
          _ -> fallBack -- just irrelevant terms
        _ -> fallBack  -- a Nothing
  where
  fallBack = return (mkCon c ci args)
  check :: Arg Term -> Dom QName -> Maybe (Maybe Term)
  check a ax = do
  -- @a@ is the constructor argument, @ax@ the corr. record field name
    -- skip irrelevant record fields by returning DontCare
    case (getRelevance a, hasElims $ unArg a) of
      (Irrelevant{}, _)   -> Just Nothing
      -- if @a@ is the record field name applied to a single argument
      -- then it passes the check
      (_, Just (_, [])) -> Nothing  -- not a projection
      (_, Just (h, e0:es0))
        | (es, Proj _o f) <- initLast1 e0 es0
        , unDom ax == f -> Just $ Just $ h es
      _                 -> Nothing

{-# SPECIALIZE isSingletonRecord :: QName -> Args -> TCM Bool #-}
-- | Is the type a hereditarily singleton record type? May return a
-- blocking metavariable.
--
-- Precondition: The name should refer to a record type, and the
-- arguments should be the parameters to the type.
isSingletonRecord :: (PureTCM m, MonadBlock m)
  => QName   -- ^ Name of record type to check.
  -> Args    -- ^ Parameters given to the record type.
  -> m Bool
isSingletonRecord r ps = isJust <$> isSingletonRecord' False r ps mempty

isSingletonRecordModuloRelevance :: (PureTCM m, MonadBlock m)
  => QName   -- ^ Name of record type to check.
  -> Args    -- ^ Parameters given to the record type.
  -> m Bool
isSingletonRecordModuloRelevance r ps = isJust <$> isSingletonRecord' True r ps mempty

-- | Return the unique (closed) inhabitant if exists.
--   In case of counting irrelevance in, the returned inhabitant
--   contains dummy terms.
isSingletonRecord'
  :: forall m. (PureTCM m, MonadBlock m)
  => Bool            -- ^ Should disregard irrelevant fields?
  -> QName           -- ^ Name of record type to check.
  -> Args            -- ^ Parameters given to the record type.
  -> Set QName       -- ^ Non-terminating record types we already encountered.
                     --   These are considered as non-singletons,
                     --   otherwise we would construct an infinite inhabitant (in an infinite time...).
  -> m (Maybe Term)  -- ^ The unique inhabitant, if any.  May contain dummy terms in irrelevant positions.
isSingletonRecord' regardIrrelevance r ps rs = do
  reportSDoc "tc.meta.eta" 30 $ vcat
    [ "Is" <+> prettyTCM (Def r $ map Apply ps) <+> "a singleton record type?"
    , "  already visited:" <+> hsep (map prettyTCM $ Set.toList rs)
    ]
  -- Andreas, 2022-03-10, issue #5823
  -- We need to make sure we are not infinitely unfolding records, so we only expand each once,
  -- and keep track of the recursive ones we have already seen.
  if r `Set.member` rs then no else do
    caseMaybeM (isRecord r) no $ \ def -> do
      -- We might not know yet whether a record type is recursive because the positivity checker hasn't run yet.
      -- In this case, we pessimistically consider the record type to be recursive (@True@).
      let recursive = maybe True (not . null) $ _recMutual def
      -- Andreas, 2022-03-23, issue #5823
      -- We may pass through terminating record types as often as we want.
      -- If the termination checker has not run yet, we pessimistically consider the record type
      -- to be non-terminating.
      let nonTerminating = maybe True not $ _recTerminates def
      reportSDoc "tc.meta.eta" 30 $ vcat
        [ hsep [ prettyTCM r, "is recursive      :", prettyTCM recursive      ]
        , hsep [ prettyTCM r, "is non-terminating:", prettyTCM nonTerminating ]
        ]
      fmap (mkCon (_recConHead def) ConOSystem) <$> do
        check (applyWhen (recursive && nonTerminating) (Set.insert r) rs) $ _recTel def `apply` ps
  where
  -- Check that all entries of the constructor telescope are singletons.
  check :: Set QName -> Telescope -> m (Maybe [Arg Term])
  check rs tel = do
    reportSDoc "tc.meta.eta" 30 $
      "isSingletonRecord' checking telescope " <+> prettyTCM tel
    case tel of
      EmptyTel -> yes
      ExtendTel dom tel -> ifM (return regardIrrelevance `and2M` isIrrelevantOrPropM dom)
        {-then-}
          (underAbstraction dom tel $ fmap (fmap (Arg (domInfo dom) __DUMMY_TERM__ :)) . check rs)
        {-else-} $ do
          caseMaybeM (isSingletonType' regardIrrelevance (unDom dom) rs) no $ \ v -> do
            underAbstraction dom tel $ fmap (fmap (Arg (domInfo dom) v :)) . check rs
  no  = return Nothing
  yes = return $ Just []

-- | Check whether a type has a unique inhabitant and return it.
--   Can be blocked by a metavar.
isSingletonType :: (PureTCM m, MonadBlock m) => Type -> m (Maybe Term)
isSingletonType t = isSingletonType' False t mempty

-- | Check whether a type has a unique inhabitant (irrelevant parts ignored).
--   Can be blocked by a metavar.
isSingletonTypeModuloRelevance :: (PureTCM m, MonadBlock m) => Type -> m Bool
isSingletonTypeModuloRelevance t = isJust <$> isSingletonType' True t mempty

isSingletonType'
  :: forall m. (PureTCM m, MonadBlock m)
  => Bool            -- ^ Should disregard irrelevant fields?
  -> Type            -- ^ Type to check.
  -> Set QName       -- ^ Non-terminating record typess we already encountered.
                     --   These are considered as non-singletons,
                     --   otherwise we would construct an infinite inhabitant (in an infinite time...).
  -> m (Maybe Term)  -- ^ The unique inhabitant, if any.  May contain dummy terms in irrelevant positions.
isSingletonType' regardIrrelevance t rs = do
    TelV tel t <- telView t
    t <- abortIfBlocked t
    addContext tel $ do
      let
        -- Easy case: η for records.
        record :: m (Maybe Term)
        record = runMaybeT $ do
          (r, ps, def) <- MaybeT $ isRecordType t
          guard $ isEtaRecordDef def
          abstract tel <$> MaybeT (isSingletonRecord' regardIrrelevance r ps rs)

        -- Slightly harder case: η for Sub {level} tA phi elt.
        -- tA : Type level, phi : I, elt : Partial phi tA.
        subtype :: m (Maybe Term)
        subtype = runMaybeT $ do
          (level, tA, phi, elt) <- MaybeT $ isCubicalSubtype t
          subin <- MaybeT $ getBuiltinName' builtinSubIn
          itIsOne <- MaybeT $ getBuiltinName' builtinIsOne
          phiV <- intervalView phi
          case phiV of
            -- If phi = i1, then inS (elt 1=1) is the only inhabitant.
            IOne -> do
              let
                argH = Arg $ setHiding Hidden defaultArgInfo
                it = elt `apply` [defaultArg (Def itIsOne [])]
              pure (Def subin [] `apply` [argH level, argH tA, argH phi, defaultArg it])
            -- Otherwise we're blocked
            OTerm phi' -> patternViolation (unblockOnAnyMetaIn phi')
            -- This fails the MaybeT: we're not looking at a
            -- definitional singleton.
            _ -> mzero

      (<|>) <$> record <*> subtype

{-# SPECIALIZE isEtaVar :: Term -> Type -> TCM (Maybe Int) #-}
-- | Checks whether the given term (of the given type) is beta-eta-equivalent
--   to a variable. Returns just the de Bruijn-index of the variable if it is,
--   or nothing otherwise.
isEtaVar :: forall m. PureTCM m => Term -> Type -> m (Maybe Int)
isEtaVar u a = runMaybeT $ isEtaVarG u a Nothing []
  where
    -- Checks whether the term u (of type a) is beta-eta-equivalent to
    -- `Var i es`, and returns i if it is. If the argument mi is `Just i'`,
    -- then i and i' are also required to be equal (else Nothing is returned).
    isEtaVarG :: Term -> Type -> Maybe Int -> [Elim' Int] -> MaybeT m Int
    isEtaVarG u a mi es = do
      (u, a) <- reduce (u, a)
      reportSDoc "tc.lhs" 80 $ "isEtaVarG" <+> nest 2 (vcat
        [ "u  = " <+> prettyTCM u
        , "a  = " <+> prettyTCM a
        , "mi = " <+> text (show mi)
        , "es = " <+> prettyList_ (map (prettyTCM . fmap var) es)
        ])
      case (u, unEl a) of
        (Var i' es', _) -> do
          guard $ mi == (i' <$ mi)
          b <- typeOfBV i'
          areEtaVarElims (var i') b es' es
          return i'
        (_, Def d pars) -> do
          guard =<< do isEtaRecord d
          fs <- map unDom . recFields . theDef <$> getConstInfo d
          is <- forM fs $ \f -> do
            let o = ProjSystem
            (_, _, fa) <- MaybeT $ projectTyped u a o f
            isEtaVarG (u `applyE` [Proj o f]) fa mi (es ++ [Proj o f])
          case (mi, is) of
            (Just i, _)     -> return i
            (Nothing, [])   -> mzero
            (Nothing, i:is) -> guard (all (== i) is) >> return i
        (_, Pi dom cod) -> addContext dom $ do
          let u'  = raise 1 u `apply` [argFromDom dom $> var 0]
              a'  = absBody cod
              mi' = fmap (+ 1) mi
              es' = (fmap . fmap) (+ 1) es ++ [Apply $ argFromDom dom $> 0]
          (-1 +) <$> isEtaVarG u' a' mi' es'
        _ -> mzero

    -- `areEtaVarElims u a es es'` checks whether the given elims es (as applied
    -- to the term u of type a) are beta-eta-equal to either projections or
    -- variables with de Bruijn indices given by es'.
    areEtaVarElims :: Term -> Type -> Elims -> [Elim' Int] -> MaybeT m ()
    areEtaVarElims u a []    []    = return ()
    areEtaVarElims u a []    (_:_) = mzero
    areEtaVarElims u a (_:_) []    = mzero
    areEtaVarElims u a (Proj o f : es) (Proj _ f' : es') = do
      guard $ f == f'
      a       <- reduce a
      (_, _, fa) <- MaybeT $ projectTyped u a o f
      areEtaVarElims (u `applyE` [Proj o f]) fa es es'
    -- These two cases can occur only when we're looking at two different
    -- variables (i.e. one of function type and the other of record type) so
    -- it's definitely not the variable we're looking for (or someone is playing
    -- Jedi mind tricks on us)
    areEtaVarElims u a (Proj{}  : _ ) (Apply _ : _  ) = mzero
    areEtaVarElims u a (Apply _ : _ ) (Proj{}  : _  ) = mzero
    areEtaVarElims u a (Proj{} : _ ) (IApply{} : _  ) = mzero
    areEtaVarElims u a (IApply{} : _ ) (Proj{} : _  ) = mzero
    areEtaVarElims u a (Apply  _ : _ ) (IApply{} : _  ) = mzero
    areEtaVarElims u a (IApply{} : _ ) (Apply  _ : _  ) = mzero
    areEtaVarElims u a (IApply{} : _) (IApply{} : _) = __IMPOSSIBLE__ -- TODO Andrea: not actually impossible, should be done like Apply
    areEtaVarElims u a (Apply v : es) (Apply i : es') = do
      ifNotPiType a (const mzero) $ \dom cod -> do
      _ <- isEtaVarG (unArg v) (unDom dom) (Just $ unArg i) []
      areEtaVarElims (u `apply` [fmap var i]) (cod `absApp` var (unArg i)) es es'


-- | Replace projection patterns by the original projections.
--
class NormaliseProjP a where
  normaliseProjP :: HasConstInfo m => a -> m a

instance NormaliseProjP Clause where
  normaliseProjP cl = do
    ps <- normaliseProjP $ namedClausePats cl
    return $ cl { namedClausePats = ps }

instance NormaliseProjP a => NormaliseProjP (x, a) where
  normaliseProjP = traverse normaliseProjP

instance NormaliseProjP a => NormaliseProjP [a] where
  normaliseProjP = traverse normaliseProjP

instance NormaliseProjP a => NormaliseProjP (Arg a) where
  normaliseProjP = traverse normaliseProjP

instance NormaliseProjP a => NormaliseProjP (Named_ a) where
  normaliseProjP = traverse normaliseProjP

instance NormaliseProjP (Pattern' x) where
  normaliseProjP p@VarP{}        = return p
  normaliseProjP p@DotP{}        = return p
  normaliseProjP (ConP c cpi ps) = ConP c cpi <$> normaliseProjP ps
  normaliseProjP (DefP o q ps) = DefP o q <$> normaliseProjP ps
  normaliseProjP p@LitP{}        = return p
  normaliseProjP (ProjP o d0)    = ProjP o <$> getOriginalProjection d0
  normaliseProjP p@IApplyP{}     = return p
